Issue1194j.agda:21,8-13
D₂ !=< D₁ of type Set
when checking that the inferred type of an application
  D₂
matches the expected type
  D₁
